@ChrisDenton : Thanks for your contribution! The author(s) have been notified to review your proposed change.

Hello, @jwmsft seems to not be responding and this has lain fallow for a year. Can we get a review from someone else? @drewbatgit or @stevewhims perhaps?

Cc @cgettys-microsoft @sivadeilra -- this came up when discussing the semantics of a Miri shim.

It was discovered that this undocumented behaviour was being relied on by a long deprecated Rust stdlib function.

FWIW this function has been un-deprecated in the mean time.

FWIW - I believe that the SAL annotations actually do match the semantics that the proposed documentation update suggests (edit: corrected misreading of the annotations) (from a recent userenv.h on my local dev machine - e.g. "C:\Program Files (x86)\Windows Kits\10\Include\10.0.22621.0\um\UserEnv.h").
I.e. lpcchSize is always written with some value, and that lpProfileDir is annotated saying that how many characters it writes are stored in that field. (the opt just means you can pass in nullptr)

SAL reference: https://learn.microsoft.com/en-us/cpp/code-quality/annotating-function-parameters-and-return-values?view=msvc-170

//=============================================================================
//
// GetUserProfileDirectory
//
// Returns the path to the root of the requested user's profile
//
// hToken         -  User's token returned from LogonUser()
// lpProfileDir   -  Receives the path
// lpcchSize      -  Size of lpProfileDir
//
// Returns:  TRUE if successful
//           FALSE if not.  Call GetLastError() for more details
//
// Note:     If lpProfileDir is not large enough or NULL, the function will fail,
//           and lpcchSize will contain the necessary buffer size.
//
// Example return value: C:\Users\Joe
//
//=============================================================================

USERENVAPI
BOOL
WINAPI
GetUserProfileDirectoryA(
    _In_                            HANDLE  hToken,
    _Out_writes_opt_(*lpcchSize)    LPSTR lpProfileDir,
    _Inout_                         LPDWORD lpcchSize);
USERENVAPI
BOOL
WINAPI
GetUserProfileDirectoryW(
    _In_                            HANDLE  hToken,
    _Out_writes_opt_(*lpcchSize)    LPWSTR lpProfileDir,
    _Inout_                         LPDWORD lpcchSize);
#ifdef UNICODE
#define GetUserProfileDirectory  GetUserProfileDirectoryW
#else
#define GetUserProfileDirectory  GetUserProfileDirectoryA
#endif // !UNICODE

Actually, I might be slightly misreading this - it may be that technically the SAL annotations don't go quite far enough - but that may just be because the annotations are pretty verbose to be that precise with:
E.g. _Out_writes_to_opt_(_Old_(*lpcchSize), *lpcchSize) might be the contract you want to have documented
Such is the challenge of writing in static analysis annotations rather than having language support (and maybe I'm missing a cleaner set of annotations for this...)

The implementation meets the requirement that you want -- on successful return, *lpcchSize is the number of WCHAR elements that have been written, including the NUL at the end.

This is strongly implied by the SAL annotations. LPWSTR itself has a SAL annotation that specifies that the pointed-to string is NUL terminated and is well-formed after function return. The _Out_writes_opt_ indicates (on the successful return) that *lpcchSize is the number of elements written to lpProfileDir. Taken together, these two invariants correctly imply that the returned string is both NUL terminated and that *lpcchSize contains its length (or is greater, which is fine).

I've checked the implementation and it guarantees this contract.